The present invention relates to techniques for solving a disjunctive system. More specifically, the invention relates to techniques that make it feasible to handle disjunctions within unification.
A number of general approaches have been proposed for solving a system such as a logical formula whose terms are equations. Some of these, such as term rewriting, operate directly on the terms, which are typically conjoined equations. Others, such as unification or merging, operate on terms converted into suitable data structures. Approaches of either of these types typically perform poorly if the system being solved includes disjunctions.
One conventional technique for handling disjunctions is to expand a system into disjunctive normal form and then solve each disjunct separately using unification. If any of the disjuncts has a consistent solution, the system is consistent and its solutions are the combined solutions of the consistent disjuncts. If none of the disjuncts has a consistent solution, the system is inconsistent and has no solutions. This technique performs poorly for a system with a large number of disjunctions, however, because the number of disjuncts in a system's disjunctive normal form increases exponentially with the number of disjunctions in the system.
Karttunen, L., "Features and Values," Proceedings of the Tenth International Conference on Computational Linguistics, Stanford University, Stanford, Calif., Jul. 2-7, 1984, pp. 28-33, discusses linguistic aspects of a general purpose facility for computing with features, where a feature may be thought of as an attribute-value pair. Pages 30-32 describe a modified unification procedure that admits disjunctive values, indicated by enclosing alternative values in braces "{}". In unifying, the disjunctive value is treated differently than an ordinary non-disjunctive value. In unifying a disjunctive value whose disjuncts are simple atomic values with a non-disjunctive simple atomic value, the result is the non-disjunctive value only if it is identical with one or the other of the disjuncts in the disjunctive value. If the disjuncts and the non-disjunctive value are all complex, on the other hand, the result is a complex disjunction indicating that either one or the other of the disjuncts is to be unified with the non-disjunctive value. Appendix A includes several further examples, of which the examples unifying "die" and "den" with "Kinder" and unifying x, y, and z illustrate unification of complex disjunctions. As shown for "(Unify x y)", a disjunct can be fully expressed in one of its occurrences, appearing in another occurrence as a pointer to the full expression.
Kasper, R. T. and Rounds, W. C., "A Logical Semantics for Feature Structures," Proceedings of the 24th Annual Meeting of the ACL, Columbia University, New York, N.Y., 1986, pp. 257-266, describe a model for unification of a feature structure such as an attribute composed of a label/value pair. Section 2 describes a complication that arises in applying Kartunnen's disjunctive values if one of the alternatives of a disjunction contains a value specified by a non-local path; constraints on alternatives of a disjunction must also apply to any non-local values contained within those alternatives. Section 4.2 defines a domain of logical formulas that describe feature structures and section 5.1 shows that the consistency problem for formulas in that domain is NP-complete if the domain includes disjunction. Therefore, any unification algorithm for formulas in that domain will almost certainly have non-polynomial worst-case complexity. Section 5.2 describes the disjunctive normal form, and points out that finding the normal form of a formula requires exponential time, where the exponent depends on the number of disjunctions in the formula. Section 5.3 describes a technique of reducing the number of disjunctions in a formula before expanding to disjunctive normal form: unifying two descriptions frequently reduces the number of terms by eliminating inconsistent terms. Section 5.4 and FIGS. 5"7 illustrate how a non-local value may be expanded to an equivalent class of paths for unification. Section 5.5 indicates that formulas containing value disjunction can be transformed into formulas containing general disjunction, but not vice versa.
Kasper, R. T., A Unification Method for Disjunctive Feature Descriptions," Proceedings of the 25th Annual Meeting of the ACL, Stanford University, Stanford, California, 1987, pp. 235-242, based on Kasper, R. T., Feature Structures: A logical Theory with Application to Language Analysis, PhD dissertation, University of Michigan, 1987, pp. 80-111, describes a method of unification by successive approximation that applies to descriptions containing general disjunction and non-local path expressions. Section 2 defines a data structure for disjunctive descriptions, a feature-description that includes a definite component and an indefinite component that is a set of disjunctions. Section 3 and FIGS. 3-6 describe the algorithm for unifying two such feature-descriptions, first by unifying their definite components, and then by examining the compatibility of their indefinite components, first checking compatibility with the unified definite components and then checking the compatibility of groups of disjuncts of different disjunctions, if any disjunctions remain. This final compatibility check is the most inefficient step, and can be used only at strategic points during a parse.
Bear, J., "Feature-Value Unification with Disjunctions," SRI International, 1987, describes a program for doing feature-value unification with directed acyclic graphs containing disjunctions, based on Karttunen's technique. Section 4 discusses the need to allow for disjunctions within disjunctions. Section 5 discusses a kind of circularity that can arise in directed acyclic graphs (dags). Section 6 discusses techniques for deciding whether a dag is consistent.
Kaplan, R. M. and Bresnan, J., "Lexical-Functional Grammar: A Formal System for Grammatical Representation," in Bresnan, J., (Ed.), The Mental Representation of Grammatical Relations, MIT Press, Cambridge, Mass., 1982, pp. 173-281 ("the LFG article"), presents a formalism for representing syntactic knowledge that is called lexical-functional grammar ("LFG"). Section 4.1 describes a sentence's functional structure ("f-structure") as encoding the sentence's meaningful grammatical relations as a set or hierarchy of ordered pairs each of which consists of an attribute and a specification of that attribute's value for the sentence. Section 4.2 sets forth the axiom that a particular attribute may have at most one value in a given f-structure. Sections 4.3 and 4.4 describe how an f-structure may be obtained from a constituent structure ("c-structure") that indicates the arrangement of words and phrases in a sentence. Section 4.4 and the Appendix describe the Locate and Merge operators, used in processing an equation derived from a functional description ("f-description") that is in turn derived from a c-structure. The Locate operator is applied to each of the sides, or designators, of an equation in the f-description to obtain the respective value of each designator. When the values have been located, the Merge operator determines whether the values are the same, hence satisfying the equality; if not, the Merge operator constructs a new entity by combining the properties of the values, provided their properties are compatible. This entity becomes the common value of the two designators. If two entities to be merged are incompatible, the Merge operator so indicates, and Section 4.5 discusses inconsistency, one type of incompatibility. The f-structures (50) and (108) illustrate representations of cooccurrences of a placeholder within an f-structure. Section 4.7 discusses long-distance dependency, with f-structures (131), (133), (143), and (169) illustrating control linkages.
De Kleer, J., Extending the ATMS," Artificial Intelligence, Vol. 28, (1986), pp. 163-196, describes an extension of the assumption-based truth maintenance system (ATMS) to handle disjunctions of assumptions. Page 163 defines environment" as a set of assumptions and defines "context" of an environment as the set of all data propositionally derivable from the assumptions using inferences, called justifications." Pages 170-173 describe disjunctions of assumptions, introducing rules to ensure label consistency and completeness. Pages 184-185 describe complex justifications, such as one of disjunctions. Pages 193-195 describe implementing disjunction, in which disjunctions are stored in a separate database. A false assumption can be removed from all disjunctions.
Mackworth, A., "Constraint Satisfaction," in Shapiro, S. C. and Eckroth, D., eds., Encyclopedia of Artificial Intelligence, New York: Wiley, 1987, pp. 205-211, describes backtracking and consistency algorithms for constraint satisfaction problems at pages 207-209.